
A high-level Petri net framework is introduced for the toxic risk assessment %of the toxic risk 
in biological and bio-synthetic systems.
Unlike empirical techniques mostly used in toxicology or toxicogenomics, we propose 
a systemic approach consisting of  a series of behavioral rules (reactions) that depend on time constraints and abstract discrete ``expression'' levels of involved agents (species).
This leads to the definition of a modular modeling environment, called \rnd for Reaction Networks with Delays, together with a suitable sound and complete abstraction allowing exhaustive verification (model-checking) of properties related to equilibrium alteration or appearing of hazardous behaviors.
The approach is applied to the study of the impact of the aspartame assimilation into the blood glucose regulation process.

%We introduce a framework to address problems related to the control of  the toxic risk in the manipulation of genes structures. 
%Most of the techniques used in this field are based on empirical analysis, we believe that toxicity can be tested in a more systematic way by exploiting the key features of this kind of applications: i.e. systems that are  governed by a series of behavioral rules (reactions) and that depend on time constraints and expression levels.
%
%We propose to work with \emph{Reaction networks with delays} or \rnd. In \rnd, systems consists of a set of species present in the environment at a given expression level. Species can degrade because of time and their presence is governed by a a set of rules (reactions). In a reaction, species can have the rôle of reactants, inhibitors or products. A reactions has a given duration, and it can take place only if all reactants are available and all  inhibitors are not for the whole duration of the reaction. Depending on the type of reaction, products are either augmented or diminished. The  dynamics of the model is given through high-level Petri nets. 
%
%As a last step, we focus on the exhaustive verification, using temporal logic, of properties linked to equilibrium breaking or unexpected appearing of unwanted behaviors. To this aim, we introduce a suitable sound and complete abstraction of \rnd.  Finally, we conclude by observing that the biologic metaphor could be adapted to a broader spectrum of  applications.